$\forall$$S$, $T$:Type, $P$, $Q$:($S$$\rightarrow\mathbb{P}$).
\\[0ex]($S$ = $T$) $\Rightarrow$ ($\forall$$z$:$S$. \{$P$($z$) $\Rightarrow$ $Q$($z$)\}) $\Rightarrow$ \{($\forall$$x$:$S$. $P$($x$)) $\Rightarrow$ ($\forall$$y$:$T$. $Q$($y$))\}